es:ES, ff:FIFO, f2f+:F2F+-decls.
plus-ify{i:l}(es;ff;is_req  ;is_ack ;awaiting ;owes_ack )
 (sndr, rcvr:ff.C, e, e':E.
 ([e: sndr is_req   rcvr]  [e: rcvr is_ack  sndr])
  ([e': sndr is_req   rcvr]  [e': rcvr is_ack  sndr])
  (e' < e)
  (x, x':E. f2f+-pred(x,e)  f2f+-pred(x',e')  (x' < x))) 

latex

Definitions	{T}, x(s), A c B, , t  T, P & Q, P  Q, P  Q, x:A. B(x), False, A, Dec(P), P  Q, P  Q
Lemmas	decidable snd-it, f2f+-pred-field, generated-thread-properties2, f2f+-pred-generates-thread, event system wf, FIFO wf, F2F+-decls wf, fifoS wf, fifoR wf, f2f+Owes wf, f2f+Wait wf, plus-ify wf, fifoC wf, f2f+Ack wf, f2f+Req wf, snd-it wf, es-causl wf, es-E wf, f2f+-pred wf, f2f+-property